
theory Executable  
imports SynLang

begin


primrec
 list_subseteq ::"'a list \<Rightarrow> 'a list \<Rightarrow> bool"  
where 
"list_subseteq [] ys = True " |
"list_subseteq (x # xs) ys = (if (x \<in>set ys) then (list_subseteq xs ys) else False)"

lemma set_list_subseteq [rule_format,code_inline] : 
  "\<forall> ys. set xs \<subseteq> set ys= list_subseteq xs ys"
by (induct xs ) (simp add : ListMem_iff)+



end
